T:Type, f:(TT), R:(TT).
retraction(T;f)
 (x:T. R(x,x))
 (x, y, z:T.
 (x = f(y))  ((x = y))  y is f*(z)  (u:T. y is f*(u)  u is f*(z)  R(u,z))  R(x,z))
 {x, y:T. x is f*(y)  R(x,y)} 

latex

Definitions	x:A  B(x), x:A. B(x), retraction(T;f), {T}, s = t, A, y is f*(x), f(a), x(s1,s2), x:AB(x), P  Q, x:A. B(x), Type, , n - m, a < b, , {x:A| B(x)} , t  T, A  B, i  j , False, #$n, -n, n+m, Void, left + right, P  Q, type List, y=f*(x) via L, , |g|, S  T, , <a, b>, hd(l), (x  l), x.A(x), x,y. t(x;y)
Lemmas	member wf, subtype rel wf, le wf, fun-connected-induction, retraction-fun-path, ge wf, nat properties, nat wf, nat ind tp, retraction wf, fun-connected wf, not wf